\begin{tabbing}
inv{-}rel($A$;$B$;$f$;${\it finv}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$a$:$A$, $b$:$B$. (${\it finv}$($b$) = (inl $a$ ) $\in$ ($A$ + Unit)) $\Rightarrow$ ($b$ = $f$($a$) $\in$ $B$))\+
\\[0ex]\& ($\forall$$a$:$A$. ${\it finv}$($f$($a$)) = (inl $a$ ) $\in$ ($A$ + Unit))
\-
\end{tabbing}